1

is it possible to run CBMC as stand alone witout Visual Express ? Do I need to recompile it or is there another trick maybe ?

I only need to use CBMC to translate a function to CNF regularly, so I want to call it with the function name, write the cnf file to disk and start again. I do not want to use Visual Studio.

Gilles 'SO- stop being evil'
  • 104,111
  • 38
  • 209
  • 254
Adrian Monk
  • 73
  • 2
  • 11

1 Answers1

2

It is entirely possible to run The CBMC model checker as a standalone program. I do it weekly on both Linux and Windows 7 :)

I'm assuming you're on Windows because of Visual Studio.

Open a command prompt and navigate to the folder where cbmc.exe is, and call it like so: cbmc --help ...to see the options you have.

The user manual has a section on how to do it, in 3.2 Command line interface. You may have to call the batch-script that sets up Visual Studio's environment for the CLI (VSVARS32.bat / vsvarsall.bat etc). On some Windows machines, that script is placed in c:\program files\microsoft visual studio\[version]\vc\bin\ if I recall correctly.

See this MSDN page for more info on that: https://msdn.microsoft.com/en-us/library/f2ccy3wt.aspx

Morten Jensen
  • 5,818
  • 3
  • 43
  • 55
  • Thank you very much. Thats the answer I have looked for. – Adrian Monk Aug 26 '15 at 20:16
  • @AdrianMonk No problem :) Have a look at the manual if you get stuck, or edit your question further if you have problems. If everything works for you, feel free to upvote and/or accept my answer. – Morten Jensen Aug 26 '15 at 21:43
  • Tusen Takk. I want to make cnf files, but need to partition then afterwards for better calculating. Did you work on this too ? Maybe Metis ? Ihave a problem to get a cnf file into Metis. – Adrian Monk Aug 28 '15 at 06:20
  • @AdrianMonk Selv tak :) No I haven't tried exporting theorems/predicates from the SMT backend, but I think it should be possible. I'm not sure about how to get them in CNF form though, but if the output is in the SMT-lib format, maybe there are other tools out there that can. I've seen your other question about this, but I can't help you much though.. May I ask what the application is ? – Morten Jensen Sep 12 '15 at 17:17