Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002020Frama-CPlug-in > pathcrawlerpublic2014-12-05 11:222015-03-17 22:18
Reporternicky 
Assigned Tomuriel 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFrama-C GIT, precise the release idFixed in VersionFrama-C Sodium 
Summary0002020: body of atomic cond belonging to an assume reproduced in sequence containing the assume
DescriptionThe ast_node.pl file generated for assert assume contains the following lines:
...
ast_node(n(24), seq, [409,n(37),n(33),422,n(48),n(44)]). % assert_assume.c: l.16
...
ast_node(n(44), assume, [atomic_cond(n(53))]). % assert_assume.c: l.17
...
atomic_cond(n(53), [n(54), 429]).
...
ast_node(n(54), seq, [422,n(48)]). % assert_assume.c: l.17

Steps To Reproducecd pathcrawler/tests/AssertAssume
frama-c -pc -pc-analyzer -lib-entry -main assert_assume assert_assume.c
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005594)
muriel (developer)
2014-12-05 14:00

si ça y est j'ai compris, les séquences sorties de la condition apparaissent 2 fois dans l'ast_node.
je regarde ça.
(0005595)
muriel (developer)
2014-12-05 15:23

[commit 43355de] dans LineaCabs

- Issue History
Date Modified Username Field Change
2014-12-05 11:22 nicky New Issue
2014-12-05 11:22 nicky Status new => assigned
2014-12-05 11:22 nicky Assigned To => muriel
2014-12-05 14:00 muriel Note Added: 0005594
2014-12-05 15:23 muriel Note Added: 0005595
2014-12-05 15:23 muriel Status assigned => resolved
2014-12-16 22:14 signoles Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
2018-11-30 10:50 signoles Category Plug-in > PathCrawler => Plug-in > pathcrawler


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker