0000259: Problem with is_finite predicate generated by -val

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000259

Frama-C

Plug-in > value analysis

public

2009-09-30 16:10

2014-02-12 16:55

Reporter

dpariente

Assigned To

pascal

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Beryllium-20090902

Target Version

Fixed in Version

Frama-C Carbon-20101201-beta1

Summary

0000259: Problem with is_finite predicate generated by -val

Description

Launching: frama-c foo.c
with foo.c (generated by "frama-c -val" on the original code) containing:

/* Generated by Frama-C */
double f(double a , double b )
{
  double t ;
  t = 0.0;
  /*@
    assert \is_finite("+", a, b);
        // synthesized
    assert \is_finite("*", a+b, a-b);
        // synthesized
    assert \is_finite("-", a, b);
        // synthesized
  */
  t = (a + b) * (a - b);
  return (t);
}

yields:
foo.c:13:[kernel] user error: syntax error while parsing annotation

which seems to be due to multiple asserts in the same @-comment.

Please note also that once the 3 asserts are 'exploded' into their own
@-comment, then "frama-c foo.c" displays:
foo.c:13:[kernel] user error: Error during annotations analysis: no such
predicate or logic function \is_finite(char *, double , double )
(but this very last point was already discussed in other threads).
Kernel seems to wait for a double typed expression parameter in \is_finite predicate, doesn't it? Like this single assert: //@ assert \is_finite((double)((a + b) * (a - b)));

Regards,
Dillon

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000426) virgile (developer) 2009-09-30 16:50	There are indeed two bugs in one - The pretty-printer should output typable code (i.e. one assert per annotation). - The assertions generated by value analysis regarding floats are still very exeperimental, and in particular there's no guarantee that they make sense with respect to ACSL standard library.

Issue History
Date Modified	Username	Field	Change
2009-09-30 16:10	dpariente	New Issue
2009-09-30 16:10	dpariente	Status	new => assigned
2009-09-30 16:10	dpariente	Assigned To	=> pascal
2009-09-30 16:50	virgile	Note Added: 0000426
2009-09-30 16:50	virgile	Status	assigned => acknowledged
2009-10-19 17:59	svn	Checkin
2010-12-02 23:13	svn	Checkin
2010-12-02 23:13	svn	Status	acknowledged => resolved
2010-12-02 23:13	svn	Resolution	open => fixed
2010-12-10 15:45	signoles	Fixed in Version	=> Frama-C Carbon-20101201-beta1
2010-12-17 19:37	signoles	Status	resolved => closed