May 10

9:21 AM
(1 post)

Doxygen

first post: PEPE89 wrote: Hi all, does anybody know how to set doxygen to skip anotations i...

May 2

7:12 PM
(6 posts)

Funtion calls modify global variables

first post: Hare wrote: Hi guys, I have a problem with my code. The function calls will l...

latest post: Hare wrote: Hi Mark, Thank you very much!! It really helps! I confused "the c...

May 2

7:03 PM
(9 posts)

_(writes) clause error VC8510

first post: PEPE89 wrote: Hi all, I got this error in simple function, I am not sure what I ...

latest post: Hare wrote: Hi Mark, Thanks very much! I added an requirement, _(requires \ma...

Apr 27

5:22 AM
(6 posts)

error VC9502: Call 'stack_free()

first post: PEPE89 wrote: Hello all, I have problem with this error: \singly_linked_list_...

latest post: MarkHillebrand wrote: Hi, the old writes clause introduced an inconsistency, which mad...

Mar 24

11:06 PM
(3 posts)

Verifying C programs with nested structures

first post: sumeshdivakaran wrote: I am trying to verify a 'C' program with nested structures. Suppose...

latest post: dtrebbien wrote: I may be mistaken on this, but objects only have one owner. An `A`...

Mar 24

10:51 PM
(5 posts)

Use of malloc and free

first post: edrdo wrote: Hello, I am having trouble understanding the verification of ca...

latest post: dtrebbien wrote: In the first case, the code is wrong. You probably meant `int* p =...

Mar 8

10:42 PM
(2 posts)

Verifying C++

first post: PEPE89 wrote: Hi all, i am trying to verify simple C++ file and iam getting fat...

latest post: dtrebbien wrote: I don't think that VCC supports C++.

Mar 5

10:44 AM
(4 posts)

Possible to declare a ghost for the value such that a given existential is satisfied?

first post: dtrebbien wrote: I am working on creating a verified implementation of strlcpy and I...

latest post: fdupress wrote: Excellent. In my experience with VCC, making proofs using assertio...

Mar 3

10:21 PM
(2 posts)

Verifying while loop

first post: PEPE89 wrote: Second problem: I need verify my function DisposeList in implemen...

latest post: dtrebbien wrote: I think that you will need `_(dynamic_owns)` and invariants on the ...

Feb 26

11:48 AM
(1 post)

error VC9731: Call to function 'printf', which has variable arguments, is not supported.

first post: PEPE89 wrote: Hi all, can anyone please help me with this error. I am not sure ...