/smoke has no effect

Feb 10, 2011 at 3:17 PM

Hello,

I typed "/2 /smoke" in the text field in Verify->Settings and activated the check mark "Active". Still, VCC successful verifies functions with contradicting preconditions, eg

_(maintains \wrapped(This))
_(writes &This->a)

I use VCC version 2.1.40210.

Regards,

Boris

Feb 10, 2011 at 4:13 PM

Hello Boris,

tried to reproduce this ...

~$ vcc /version
Microsoft Research Vcc Version 2.1.40210.0
Microsoft Research Boogie Version 2.1.21217.0
Microsoft Research Z3 Version 2.0.41203.1
~$ cat test2.c 
#include "vcc.h"
typedef struct B_str {
    unsigned int a;
} B_t;
void test (B_t *b) 
_(maintains \wrapped(b))
_(writes &b->a)
{
};
~$ vcc /2 test2.c  
Verification of test succeeded.
~$ vcc /2 /smoke test2.c  
Verification of test succeeded.
C:\cygwin\home\hbl3\test2.c(7): found unreachable code, possible soundness violation, please check the axioms or add an explicit assert(false)
Maybe I missed sth?

Holger

Feb 11, 2011 at 8:36 AM

Hello Holger,

I use the VS 2008 plugin and the context menu "Verify function". The message "found unreachable code, possible soundness violation" doesn't appear in the GUI.

Boris

Editor
Feb 11, 2011 at 8:40 AM
I just gave it a try to make sure that it wasn't a problem with the plugin ignoring the cli option, and it doesn't appear to be: the command line call does include the /smoke.
Can you confirm that the command line call displayed in the output window includes the /smoke option? Maybe VCC just forgets to display the output...

On Fri, Feb 11, 2011 at 9:36 AM, borishollas <notifications@codeplex.com> wrote:

From: borishollas

Hello Holger,

I use the VS 2008 plugin and the context menu "Verify function". The message "found unreachable code, possible soundness violation" doesn't appear in the GUI.

Boris

Read the full discussion online.

To add a post to this discussion, reply to this email (VCC@discussions.codeplex.com)

To start a new discussion for this project, email VCC@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe or change your settings on codePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at codeplex.com


Coordinator
Feb 11, 2011 at 8:44 AM

Hi Boris,

  I am seeing the message in the VCC output window (View -> Output, Show Output from "Verification"). I'm afraid this might be the only place this currently shows up; there should probably be a prominent warning elsewhere.

  Regards, Mark