Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002123Frama-CPlug-in > wppublic2015-06-01 12:422015-06-29 16:55
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformSodium-20150201OSOS Versionxubuntu14.04
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002123: validity of obligation from statement contract depends on whether the statement is enclosed in block {}
DescriptionRunning "frama-c -wp 480.c" on the attached program produces one unproven Alt-Ergo obligation (see file "in_block_foo_stmt_post_Alt-Ergo.mlw"). If the block parentheses in line 16 and 23 are removed, the corresponding obligation (file "not_in_block_foo_stmt_post_Alt-Ergo.mlw") is proven. The differences between both obligations files are: 772c772 < forall t_2,t_1 : (addr,int) farray. --- > forall t_1 : (addr,int) farray. 780c780 < (1 = L_deref(t_2, a)) --- > (1 = L_deref(t_1, a)) So, enclosing the statement in a block apparently creates an unrelated memory state.
TagsNo tags attached.
Attached Filesc file icon 480.c [^] (311 bytes) 2015-06-01 12:42 [Show Content]
? file icon in_block_foo_stmt_post_Alt-Ergo.mlw [^] (31,027 bytes) 2015-06-01 12:42
? file icon not_in_block_foo_stmt_post_Alt-Ergo.mlw [^] (31,023 bytes) 2015-06-01 12:42

- Relationships

-  Notes
(0005952)
correnson (manager)
2015-06-29 16:54

This is very surprising, It seems that labels in function calls are not correctly treated.
(0005953)
correnson (manager)
2015-06-29 16:55

I must investigate the problem.

- Issue History
Date Modified Username Field Change
2015-06-01 12:42 Jochen New Issue
2015-06-01 12:42 Jochen Status new => assigned
2015-06-01 12:42 Jochen Assigned To => correnson
2015-06-01 12:42 Jochen File Added: 480.c
2015-06-01 12:42 Jochen File Added: in_block_foo_stmt_post_Alt-Ergo.mlw
2015-06-01 12:42 Jochen File Added: not_in_block_foo_stmt_post_Alt-Ergo.mlw
2015-06-29 16:54 correnson Note Added: 0005952
2015-06-29 16:55 correnson Note Added: 0005953
2015-06-29 16:55 correnson Status assigned => acknowledged


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker