Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002412Frama-CPlug-in > RTEpublic2018-12-03 18:312018-12-03 19:49
Reporterrmalak 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusconfirmedResolutionopen 
Platformx86_64OSLinux x86_64OS VersionDebian Sid
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002412: E-ACSL crash with RTE generated assertion with booleans
DescriptionThere might be a regression with the RTE or E-ACSL plugin with Argon.

/////////// boolean.c

#include <stdbool.h>

bool return_false(void)
{
  return false;
}

int main(void)
{
  return 0;
}
///////////////////////////
Steps To ReproduceOn Argon 18.0 (2f7a0eee0) :

$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false

$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Current source was: rte_boolean.c:10
  The full backtrace is:
  Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
  Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
  Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
  Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
  Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
  Called from file "queue.ml", line 105, characters 6-15
  Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
  
  Unexpected error (Stack overflow).
  Please report as 'crash' at http://bts.frama-c.com/. [^]
  Your Frama-C version is 18.0 (Argon).
  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 InformationOn Chlorine-20180502 (bfd93b819) :

$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false

$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
TagsNo tags attached.
Attached Filesc file icon boolean.c [^] (118 bytes) 2018-12-03 18:31 [Show Content]

- Relationships

-  Notes
(0006687)
signoles (manager)
2018-12-03 19:01

Thank you for the report.

In 18-Argon, the RTE plug-in generates additional annotations in order to check that no trap representations are read from _Bool lvalues. These properties were not generated before 18-Argon, but are unfortunately not yet well supported by E-ACSL (as you experimented).

Using -no-warn-invalid-bool would result in the 17-Chlorine's behaviour.

$ frama-c -no-warn-invalid-bool -machdep x86_64 boolean.c -rte -then -e-acsl -then-last -print
<all is fine>
(0006688)
rmalak (reporter)
2018-12-03 19:49

Hi,
Thanks for the quick answer !
R.

- Issue History
Date Modified Username Field Change
2018-12-03 18:31 rmalak New Issue
2018-12-03 18:31 rmalak Status new => assigned
2018-12-03 18:31 rmalak Assigned To => signoles
2018-12-03 18:31 rmalak File Added: boolean.c
2018-12-03 19:01 signoles Note Added: 0006687
2018-12-03 19:01 signoles Status assigned => confirmed
2018-12-03 19:49 rmalak Note Added: 0006688


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker