Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000793Frama-CPlug-in > wppublic2011-04-13 13:442013-04-19 11:05
Reporterpatrick 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000793: time too long even with -wp-timeout 1
DescriptionThe PO is quickly computed, but the proof seems to take a llong time, but -wp-timeout 1 has no effect.
Additional InformationRevision: 12840
> frama-c valinit.c -wp -wp-prop p4 -wp-proof alt-ergo -wp-timeout 1
TagsNo tags attached.
Attached Filesc file icon valinit.c [^] (3,663 bytes) 2011-04-13 13:44 [Show Content]

- Relationships

-  Notes
(0001780)
patrick (developer)
2011-04-14 09:56

The problem comes from a combinational explosion when expanding the 'let' constructs before calling the prover.
(0001916)
dargaye (developer)
2011-05-20 13:43

from alt-ergo
(0003753)
correnson (manager)
2013-03-12 13:18

Timeout 12s with wp-par 1 is now ok.
Using -wp-model ref makes each PO discharged in less than 4s.
(0003754)
correnson (manager)
2013-03-12 13:18

Together with issue 0000794.

- Issue History
Date Modified Username Field Change
2011-04-13 13:44 patrick New Issue
2011-04-13 13:44 patrick Status new => assigned
2011-04-13 13:44 patrick Assigned To => dargaye
2011-04-13 13:44 patrick File Added: valinit.c
2011-04-14 09:56 patrick Note Added: 0001780
2011-05-20 13:43 dargaye Note Added: 0001916
2011-05-20 13:43 dargaye Status assigned => closed
2011-05-20 13:43 dargaye Resolution open => fixed
2013-03-12 13:18 correnson Note Added: 0003753
2013-03-12 13:18 correnson Note Added: 0003754
2013-03-12 13:18 correnson Status closed => resolved
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