Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:32 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002338Frama-CPlug-in > wppublic2020-02-17 18:08
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionduplicate 
PlatformSulfur-20171101OSUbuntu 17.04OS Version
Product Version 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002338: \false provable from recursive logic definition
DescriptionRunning "frama-c -wp foo.c -wp-prover alt-ergo -wp-prover eprover" on the attached file proves all goals, including a lemma "Check" which just says "\false", from nothing but a recursive definition of a logic int function.
The latter is well-founded since its only recursive call uses a parameter value n==0 which immediately employs the base case.

The problem disappears
(1) when "integer" is used as result type and as 3rd parameter type,
(2) when "a[]" is omitted,
(3) when lemma "Alpha" is renamed to a name lexicographically after "Check", or
(4) when "cvc3" or "cvc4-15" is used instead of "eprover".
The problem remains, however, when "z3" is used.
TagsNo tags attached.
Attached Files
  • c file icon foo.c (220 bytes) 2017-12-18 12:43 -
    /*@
      logic int
        Acc{L}(int* a, integer n, int init) =
          ((n <= 0) ? init : (int)(Acc{L}(a,0,init) + a[0]));
    */
    
    /*@
      lemma AInit{L}: \forall int *a, init; Acc{L}(a,0,init) == init;
      lemma Check: \false;
    */
    
    
    
    
    c file icon foo.c (220 bytes) 2017-12-18 12:43 +
  • txt file icon diff.txt (1,575 bytes) 2017-12-18 13:28 -
    diff -r outA/typed/Axiomatic.why outD/typed/Axiomatic.why
    26a27,28
    > lemma Q_Check: false
    > 
    34c36
    < lemma Q_AInit:
    ---
    > lemma Q_DInit:
    39,40d40
    < 
    < lemma Q_Check: false
    diff -r outA/typed/lemma_AInit_Alt-Ergo.mlw outD/typed/lemma_AInit_Alt-Ergo.mlw
    817c817
    < (* --- Lemma 'AInit'                                      --- *)
    ---
    > (* --- Lemma 'DInit'                                      --- *)
    831c831
    < goal lemma_AInit:
    ---
    > goal lemma_DInit:
    diff -r outA/typed/lemma_AInit_Alt-Ergo.out outD/typed/lemma_AInit_Alt-Ergo.out
    1c1
    < File "outA/typed/lemma_AInit_Alt-Ergo.mlw", line 832, characters 3-113:Valid (0.0200) (15 steps)
    ---
    > File "outD/typed/lemma_DInit_Alt-Ergo.mlw", line 832, characters 3-113:Valid (0.0200) (15 steps)
    diff -r outA/typed/lemma_AInit.ergo outD/typed/lemma_AInit.ergo
    2c2
    < (* --- Lemma 'AInit'                                      --- *)
    ---
    > (* --- Lemma 'DInit'                                      --- *)
    16c16
    < goal lemma_AInit:
    ---
    > goal lemma_DInit:
    diff -r outA/typed/lemma_Check_Alt-Ergo.mlw outD/typed/lemma_Check_Alt-Ergo.mlw
    831c831
    < axiom Q_AInit:
    ---
    > axiom Q_DInit:
    diff -r outA/typed/lemma_Check_Alt-Ergo.out outD/typed/lemma_Check_Alt-Ergo.out
    1c1
    < File "outA/typed/lemma_Check_Alt-Ergo.mlw", line 837, characters 19-24:I don't know (0.0240) (10 steps)
    ---
    > File "outD/typed/lemma_Check_Alt-Ergo.mlw", line 837, characters 19-24:I don't know (0.0240) (10 steps)
    diff -r outA/typed/lemma_Check.ergo outD/typed/lemma_Check.ergo
    16c16
    < axiom Q_AInit:
    ---
    > axiom Q_DInit:
    Only in outA/typed: lemma_Check_Why3_eprover.out
    
    txt file icon diff.txt (1,575 bytes) 2017-12-18 13:28 +
  • ? file icon eprover.input (3,591 bytes) 2017-12-18 16:55

-Relationships
child of 0002427acknowledgedcorrenson Prove of \false 
+Relationships

-Notes

~0006492

Jochen (reporter)

The naming dependance (3) reminds me to the closed issue 0002237, where ordering of goals was involved, too. Maybe both issues are related?

~0006493

Jochen (reporter)

Trying to track down the naming dependence (3) somewhat further, I ran the above command with "-wp-out outA" added on the original file "foo.c", and with "-wp-out outD" on a modification of "foo.c" where "AInit" was renamed to "DInit". Then I renamed the files in "outD/typed" appropriately (e.g. "lemma_DInit.ergo" to "lemma_AInit.ergo"), and ran "diff -r outA outD >diff.txt" (attached).

It appears to me the only difference is in file "Axiomatic.why" where the order is "Q_TL_Acc, Q_AInit, Q_Check" in outA/, but "Q_Check, Q_TL_Acc, Q_DInit" in outD/.

~0006495

correnson (manager)

Yes I think the order / dependency problem is harmful here... Thanks for the inputs, it would help to fix the entire problem.

~0006498

Jochen (reporter)

I managed to intercept the input given to eprover, and to boil it down to the version in "eprover.input" (attached).

The call "eprover -s -R -xAuto -tAuto --cpu-limit=10 --tstp-in eprover.input" (options as observed from the call by why3) results in "$false" being proven. None of the axioms can be deleted without losing the provability.

A strange list of predicates is involved in the inconsistency, viz.
    base from_int get included infix_ls infix_lseq infix_pl infix_pl1 is_sint32 is_uint32 l_Acc mk_addr mod offset prefix_mn prefix_mn1 separated shift to_sint32 to_uint32 truncate valid_rd valid_rw
(generated from "eprover.input"). Intersting enough, the translation of the lemma "AInit" doesn't appear in the file. It seems that this lemma is needed in the C source only to ensure inclusion of some axioms that participate in the inconsistency.

~0006756

evdenis (reporter)

If the return value type of Acc will be changed from "int" to "integer" then contradiction disappears. Similar bug https://bts.frama-c.com/view.php?id=2427
I think that maybe it is possible to extract the exact steps to contradiction with z3, because it's very hard to understand eprover output.

~0006757

evdenis (reporter)

> "translation of the lemma "AInit" doesn't appear in the file"

For me it seems like the definition of Acc is self-contradictionary. Definitely Eprover tries to use different values beyond the bounds of the int type.

~0006758

virgile (developer)

The situation is slightly different from the one in 2427. In 2427, we had an axiom that compared an int (implicitly converted into integer) with a (potentially outside of the int range) integer. Here, we explicitly convert an integer into an int, which has a perfectly defined semantics in ACSL. Hence, I'd say there's no inherent contradiction as far as ACSL is concerned (the semantics of Acc might not be the one the user has in mind, but that's a different story). in particular,

/*@ lemma AOne{L}: \forall int* a, init; Acc{L}(a,1,init) == a[0] + init; */

should not be provable, and it appears not to be: in the TIP, we can unfold the definition of L_Acc twice to obtain a goal of the form x = to_sint32(x), for x a sum of two int32 (i.e. potentially outside the range of int32) while the axiomatic of the to_sint32 builtin allows this equality only if x is within bounds (axiom id_sint32 in the WP arithmetic model).

~0006895

correnson (manager)

The *only* remaining problem is the one for https://bts.frama-c.com/view.php?id=2427
Actually, a guard is missing in the definition of the predicate to cope with the "int" parameter to be small enough.

~0006896

correnson (manager)

Partially solved (order of declaration)
Remains duplicate of another issue

~0006944

signoles (manager)

Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2017-12-18 12:43 Jochen New Issue
2017-12-18 12:43 Jochen Status new => assigned
2017-12-18 12:43 Jochen Assigned To => correnson
2017-12-18 12:43 Jochen File Added: foo.c
2017-12-18 12:57 Jochen Note Added: 0006492
2017-12-18 13:28 Jochen Note Added: 0006493
2017-12-18 13:28 Jochen File Added: diff.txt
2017-12-18 14:59 correnson Note Added: 0006495
2017-12-18 16:55 Jochen Note Added: 0006498
2017-12-18 16:55 Jochen File Added: eprover.input
2019-03-09 13:45 evdenis Note Added: 0006756
2019-03-09 13:50 evdenis Note Added: 0006757
2019-03-11 11:26 virgile Note Added: 0006758
2019-10-17 15:29 correnson Note Added: 0006895
2019-10-17 15:29 correnson Relationship added child of 0002427
2019-10-17 15:30 correnson Note Added: 0006896
2019-10-17 15:30 correnson Status assigned => resolved
2019-10-17 15:30 correnson Resolution open => duplicate
2020-02-17 18:06 signoles Fixed in Version => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006944
+Issue History