Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000640Frama-CPlug-in > wppublic2010-12-16 11:262011-05-19 13:36
Reporterholgerblasum 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101201-beta1 
Target VersionFrama-C Nitrogen-20111001Fixed in Version 
Summary0000640: Issue INSTALL guidance that alt-ergo has to be up-to-date (0.92 apparently)
DescriptionThis might a bit too picky but in case it is useful for the new release ... When I updated to the new release first I hadn't updated alt-ergo (it's fine with 0.92.2 but not with 0.91). Others will run into that too ... Simply point out that dependency in the release notes ("INSTALL" in the root is where I would look). Below is output generated from alt-ergo 0.92.2; 0.91; 0.9. $ alt-ergo -version Alt-Ergo 0.92.2 $ frama-c -wp -proof alt-ergo swap.c swap1.c [kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20101201-b1). Aorai; Jessie [kernel] preprocessing with "gcc -C -E -I. swap.c" [kernel] preprocessing with "gcc -C -E -I. swap1.c" [wp] warning: Missing RTE guards [wp] [Alt-Ergo] Goal store_swap_post_2_B : Valid [wp] [Alt-Ergo] Goal store_swap_post_1_A : Valid $ alt-ergo -version Alt-Ergo 0.91 $ frama-c -wp -wp-proof alt-ergo swap.c swap1.c [kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20101201-beta1). Aorai; Jessie [kernel] preprocessing with "gcc -C -E -I. swap.c" [kernel] preprocessing with "gcc -C -E -I. swap1.c" [wp] warning: Missing RTE guards alt-ergo -arrays /tmp/store_swap_post_2_B0f5276.why File "/tmp/store_swap_post_2_B0f5276.why", line 298, characters 3-4:syntax error [wp] [Alt-Ergo] Goal store_swap_post_2_B : Failed File "/tmp/store_swap_post_1_Add7b47.why", line 298, characters 3-4:syntax error [wp] [Alt-Ergo] Goal store_swap_post_1_A : Failed $ alt-ergo -version Alt-Ergo 0.9 $ frama-c -wp -wp-proof alt-ergo swap.c swap1.c [kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20101201-beta1). Aorai; Jessie [kernel] preprocessing with "gcc -C -E -I. swap.c" [kernel] preprocessing with "gcc -C -E -I. swap1.c" [wp] warning: Missing RTE guards alt-ergo -arrays /tmp/store_swap_post_2_B5e2f18.why [wp] [Alt-Ergo] Goal store_swap_post_2_B : Failed [wp] [Alt-Ergo] Goal store_swap_post_1_A : Failed
TagsNo tags attached.
Attached Files

- Relationships
parent of 0000641closeddargaye alt-ergo version managment 

-  Notes
(0001312)
dargaye (developer)
2010-12-16 13:28

The officialy supported alt-ergo version is 0.92.2, as mentionned in the WP plug-in manual (p.17). As explained in the manual, WP should also work with alt-ergo 0.91.x , provided option -wp-no-arrays is used.
(0001313)
signoles (manager)
2010-12-16 13:33
edited on: 2010-12-16 13:34

I agree it seems to be an issue with alt-ergo 0.91 and plug-in Wp (not tested myself if the issue is reproducible). But the INSTALL file does not handle specific plug-in dependencies like alt-ergo. Its section "Requirements" explicitely says that "Plug-ins may have their own requirements. Consult their specific documentations for details."
(0001913)
correnson (manager)
2011-05-19 13:36

Cf BTS 641

- Issue History
Date Modified Username Field Change
2010-12-16 11:26 holgerblasum New Issue
2010-12-16 11:26 holgerblasum Status new => assigned
2010-12-16 11:26 holgerblasum Assigned To => dargaye
2010-12-16 13:28 dargaye Note Added: 0001312
2010-12-16 13:28 dargaye Status assigned => closed
2010-12-16 13:28 dargaye Resolution open => no change required
2010-12-16 13:33 signoles Note Added: 0001313
2010-12-16 13:34 signoles Note Edited: 0001313
2010-12-16 13:38 dargaye Status closed => feedback
2010-12-16 13:38 dargaye Resolution no change required => reopened
2010-12-16 13:42 dargaye Relationship added parent of 0000641
2010-12-16 14:59 signoles Status feedback => acknowledged
2011-01-28 11:43 correnson Target Version => Frama-C Nitrogen-20110901
2011-05-19 13:36 correnson Note Added: 0001913
2011-05-19 13:36 correnson Status acknowledged => closed
2011-05-19 13:36 correnson Resolution reopened => fixed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker