Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000992Frama-CPlug-in > wppublic2011-10-20 14:372013-04-19 11:05
ReporterAnne 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000992: Wrong WP computation when calling a function with behaviors (assigns problem ?)
DescriptionThe assert [0==1] is proved Valid in the enclosed example. This is because the proof obligation has an hypothesis [b = b + 1] instead of [b = b' + 1].

This problem appears from rev 15799 which is about [assigns] :
[WP] Warning for missing assigns clauses + better merge of assigns for function calls

Additional Information$ frama-c toto.c -wp -wp-prop F -wp-print -wp-no-simpl

Proof Obligation assert_1_F:
Prover Alt-Ergo returns Valid
Environment: Store_env1
 - Assumes Post-condition for 'end' (file toto.c, line 10) of 'add'
 - Assumes Post-condition for 'ok' (file toto.c, line 6) of 'add'
 + Proves Assertion 'F' (file toto.c, line 19)
Goal store_f_assert_1_F:
  let bound_0 = 0 in
  let bound_1 = bound_0 in
  ((1000 <= bound_1) ->
   false) ->
  ((bound_1 < 1000) ->
   (bound_0 = (bound_1+1))) ->
  tag_F:(0 = 1)
TagsNo tags attached.
Attached Filesc file icon toto.c [^] (312 bytes) 2011-10-20 14:37 [Show Content]

- Relationships

-  Notes
(0002403)
Anne (reporter)
2011-10-20 15:58

Loïc told me that he understand the problem and try to fix it.

A workaround is to use a global [assigns] property instead of specifying them in the behaviors. In my cases, it works.
(0003745)
yakobowski (manager)
2013-03-10 00:09

Seems to have been fixed at some point, perhaps thanks to Typed model.

- Issue History
Date Modified Username Field Change
2011-10-20 14:37 Anne New Issue
2011-10-20 14:37 Anne Status new => assigned
2011-10-20 14:37 Anne Assigned To => correnson
2011-10-20 14:37 Anne File Added: toto.c
2011-10-20 15:58 Anne Note Added: 0002403
2013-03-10 00:09 yakobowski Note Added: 0003745
2013-03-10 00:09 yakobowski Status assigned => resolved
2013-03-10 00:09 yakobowski Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker