Verified software toolchain: if-then-else proof

Question

I'm learning using the Verified Software Toolchain (VST). I get stuck at proving a simple "if-then-else" block.

Here is the .c file:

int iftest(int a){
   int r=0; 
   if(a==2){
      r=0;
   else{
      r=0;
   }
return r;
}

I write a specification about the iftest() as follow:

Definition if_spec :=`
DECLARE _iftest`
      WITH a0:int
                PRE [_a OF tint]
                PROP ()
                LOCAL (`(eq (Vint a0)) (eval_id _a))
                SEP ()
                POST [tint]
                PROP ()
                LOCAL ((`(eq (Vint (Int.repr 0))) retval))
                SEP ().`

the proof steps are:

Lemma body_iftest : semax_body Vprog Gtot f_iftest if_spec.Proof. start_function. name a _a. name r _r. forward. (*r=0*) simplify_typed_comparison. forward. (*if(E)*). go_lower. subst. normalize.

it generates a hypothesis:Post := EX x : ?214, ?215 x : environ -> mpred and the "then" clause can't go on by "go_lower" and "normalize".

I never used VST (actually it's the first time I hear about it). You might have more feedback on their own mailing-list, or on the Coq mailing list: https://sympa.inria.fr/sympa/arc/coq-club . — Vinz, Aug 27 '13 at 12:57
@Vinz VST does not have a mailing list for now, but they recently created a tag `verifiable-c` for questions on SO — Necto, Jan 11 '15 at 18:27

score 1 · Answer 1 · answered Jan 11 '15 at 18:24

In the current version of VST there is a forward_if PRED tactic. Here is how you can use it to solve your goal:

Require Import floyd.proofauto.
Require Import iftest.

Local Open Scope logic.
Local Open Scope Z.

Definition if_spec :=
  DECLARE _iftest
      WITH a0:int
                PRE [_a OF tint]
                PROP ()
                LOCAL (`(eq (Vint a0)) (eval_id _a))
                SEP ()
                POST [tint]
                PROP ()
                LOCAL ((`(eq (Vint (Int.repr 0))) retval))
                SEP ().

Definition Vprog : varspecs := nil.
Definition Gtot : funspecs := if_spec :: nil.

Lemma body_iftest : semax_body Vprog Gtot f_iftest if_spec.
Proof.
  start_function.
  name a _a.
  name r _r.
  forward.
  forward_if (PROP ()
                   LOCAL (`(eq (Vint (Int.repr 0))) (eval_id _r)) SEP()). 
  + forward.
    entailer.
  + forward.
    entailer.
  + forward.
Qed.

P.S. @bazza is right about a missing } before else. I assume it is fixed.

score 0 · Answer 2 · answered Aug 27 '13 at 22:10

0

Potentially a non-helpful answer, but I can't help noticing that your .c code has 3 {'s and only 2 }'s, suggesting that it doesn't compile. Could the error message you're receiving have something to do with that?

answered Aug 27 '13 at 22:10

bazza

7,580
15
22

1

Yeah, he's missing the "}" before the "else". With that added, the function boils down to return 0;, so I'm not entirely sure what the point of any of it is. I'm guessing he typed up a fabricated example real quick and got a few bits wrong in the moment. – Pegasus Epsilon Aug 29 '13 at 06:57

Verified software toolchain: if-then-else proof

2 Answers2