Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0002501Frama-CPlug-in > wppublic2020-03-10 11:442020-06-12 08:59
Reporterjens 
Assigned ToAllanBlanchard 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSLinux, macOSOS Version
Product VersionFrama-C 20-Calcium 
Target VersionFixed in VersionFrama-C 21-Scandium 
Summary0002501: error in generated proof obligation
DescriptionThe attached file 'issue.c' contains a simplified (but still not very small) example of an issue I have within ACSL by Example.

There is lemma R_2 for the logic function R.
The definition of R uses the logic function F contained in the axiomatic block A.
When trying to verify R_2 with the command line below I obtain the message
                  [Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")

frama-c -wp -wp-prover alt-ergo -wp-prover native:coq issue.c
[kernel] Parsing issue.c (with preprocessing)
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Failed] Goal typed_lemma_R_2
  Alt-Ergo 2.3.1: Failed
                  [Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
       Coq: Unknown
[wp] [Cache] found:1
[wp] Proved goals: 1 / 2
  Qed: 0
  Coq: 0 (unknown: 1)
  Alt-Ergo 2.3.1: 1 (10ms) (23) (cached: 1) (failed: 1)


When looking at the generated verification condition with Coq I found the following:
The generated hypothesis 'FixL_R' uses of course the function 'L_F'.
However, the necessary import clause 'Require Import A_A.' comes only AFTER the definition of 'FixL_R'.

Additional InformationThere is a work-around by calling the helper function 'Fix' in the definition of R (see the comment in the code).

The problem also "disappears' if lemma 'R_1' is removed (but I don't have this option).

While looking at this problem, I noticed that in general coq definitions and import clauses are interspersed in the verification conditions...
TagsNo tags attached.
Relationships
Attached Filesc issue.c (857) 2020-03-10 11:44
https://bts.frama-c.com/file_download.php?file_id=1347&type=bug

Notes
(0006971)
jens   
2020-05-09 16:45   
With 20.0+dev (Calcium), installed early May 2020 from https://git.frama-c.com/pub/frama-c, the error is still present.
(0006972)
AllanBlanchard   
2020-05-12 17:12   
(Last edited: 2020-05-12 17:27)
The problem has been fixed. The fix will be available in the next release (and in the upcoming bêta) but not immediately in the public development version.

Issue History
Date ModifiedUsernameFieldChange
2020-03-10 11:44jensNew Issue
2020-03-10 11:44jensStatusnew => assigned
2020-03-10 11:44jensAssigned To => correnson
2020-03-10 11:44jensFile Added: issue.c
2020-03-16 12:32corrensonAssigned Tocorrenson => AllanBlanchard
2020-05-09 16:46jensNote Added: 0006971
2020-05-12 17:12AllanBlanchardNote Added: 0006972
2020-05-12 17:12AllanBlanchardStatusassigned => resolved
2020-05-12 17:12AllanBlanchardFixed in Version => Frama-C 21-Scandium
2020-05-12 17:12AllanBlanchardResolutionopen => fixed
2020-05-12 17:27AllanBlanchardNote Edited: 0006972bug_revision_view_page.php?bugnote_id=6972#r458
2020-06-12 08:59signolesStatusresolved => closed