Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001922Frama-CPlug-in > wppublic2014-09-12 15:342015-03-17 22:18
Reporterlapawczykt 
Assigned Tocorrenson 
PriorityurgentSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSxubuntuOS Version14.04
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001922: WP-Plugin crashes due to an internal error
DescriptionWhen the attached file is called with the command line, that reads as follows:

frama-c.byte -pp-annot -no-unicode -wp -wp-no-bits -wp-rte -wp-script 'wp0.script' -wp-model Typed+ref -wp-out foo.wp foo.c

Frama-C produces the following output:

[kernel] preprocessing with "gcc -C -E -I. -dD foo.c"
Adhesion_Factor.c:1:0: warning: "__STDC__" redefined [enabled by default]
 /* =============================================================================
 ^
foo.c:1:0: note: this is the location of the previous definition
 # 1 "Adhesion_Factor.c"
 ^
Adhesion_Factor.c:1:0: warning: "__STDC_HOSTED__" redefined [enabled by default]
 /* =============================================================================
 ^
foo.c:1:0: note: this is the location of the previous definition
 # 1 "Adhesion_Factor.c"
 ^
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function TrackToTrain_Packet_071
[rte] annotating function TrackToTrain_Packet_071_Encoder
[wp] Collecting variable usage
[wp] Computing [100 goals...]
[wp] failure: Non-assignable term (P_Telegram+(0 .. I_Cur_Dim-1))
[kernel] Current source was: Adhesion_Factor.c:59
         The full backtrace is:
         Raised at file "src/kernel/log.ml", line 524, characters 30-31
         Called from file "src/kernel/log.ml", line 518, characters 9-16
         Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
         Called from file "list.ml", line 55, characters 20-23
         Called from file "set.ml", line 304, characters 38-41
         Called from file "map.ml", line 168, characters 20-25
         Called from file "map.ml", line 168, characters 10-18
         Called from file "map.ml", line 168, characters 10-18
         Called from file "src/lib/bag.ml", line 96, characters 16-24
         Called from file "src/lib/bag.ml", line 96, characters 16-24
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 37, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
         Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
         
         Plug-in wp aborted: internal error.
         Please report as 'crash' at http://bts.frama-c.com/. [^]
         Your Frama-C version is Neon-20140301.
         Note that a version and a backtrace alone often do not contain enough
         information to understand the bug. Guidelines for reporting bugs are at:
         http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines [^]
Additional InformationThe attached foo.c is the preprocessed version of a file out of the openETCS project. All used predicates are already included in the file.
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (97,160 bytes) 2014-09-12 15:34 [Show Content]

- Relationships

-  Notes
(0005453)
signoles (manager)
2014-09-12 16:06

Thanks for your report. This crash is actually already fixed in the current development version.

With the current version, you get the following error message. It means that an assigns clause about P_Telegram+(0 .. I_Cur_Dim-1) is probably missing in one of your specifications (or there is an issue with your postcondition). I actually add such an assigns in your code, and now I get the same error message in another place of your code... I let you debug your spec forward :).

=====
Adhesion_Factor.h:91:[wp] user error: Non-assignable term (P_Telegram+(0 .. I_Cur_Dim-1))
[kernel] Plug-in wp aborted: invalid user input.
=====
(0005454)
virgile (developer)
2014-09-12 16:57

To complete Julien's answer:

- the error is not due to a missing assigns, but to an incorrect assigns: in your TrackToTrain_Packet_071_Encoder function, the assigns clause should read

    assigns P_Telegram[0 .. I_Cur_Dim-1];

Indeed, you want to assigns the cells of the array (assigns p means that you might modify the value of p, not the one of *p). As a matter of fact, this error ought to be reported by the kernel instead of the WP, as this is a syntactic error: arguments of assigns clause must be lvalues.

With this change, wp runs fine on your file, with 95/161 goals proved.

- Issue History
Date Modified Username Field Change
2014-09-12 15:34 lapawczykt New Issue
2014-09-12 15:34 lapawczykt Status new => assigned
2014-09-12 15:34 lapawczykt Assigned To => correnson
2014-09-12 15:34 lapawczykt File Added: foo.c
2014-09-12 16:06 signoles Note Added: 0005453
2014-09-12 16:06 signoles Status assigned => resolved
2014-09-12 16:06 signoles Resolution open => fixed
2014-09-12 16:57 virgile Note Added: 0005454
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker