2021-01-15 15:08 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002382Frama-CKernelpublic2019-07-05 11:41
Reporterevdenis 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C 19-Potassium 
Summary0002382: handling of escape sequences
DescriptionCode:
/*@
   predicate isspace(integer c)  = c == ' '  || c == '\f' || c == '\n' ||
                                                       c == '\r' || c == '\t' || c == '\v';
 */


Error:
[kernel] Parsing test.h (with preprocessing)
test.h:2:[kernel] failure: Unknown error (File "src/kernel_internals/parsing/logic_lexer.mll", line 390, characters 20-26: Assertion failed)


Need to support '\v'.
TagsNo tags attached.
Attached Files
  • c file icon escape_sequences.c (154 bytes) 2018-07-04 09:15 -
    /*@
       predicate isspace(integer c)  = c == ' '  || c == '\f' || c == '\n' ||
                                       c == '\r' || c == '\t' || c == '\v';
     */
    
    c file icon escape_sequences.c (154 bytes) 2018-07-04 09:15 +

-Relationships
+Relationships

-Notes

~0006567

evdenis (reporter)

Found in version: Chlorine-20180501

~0006574

virgile (developer)

Fixed in some development branch. Most likely part of Frama-C Argon
+Notes

-Issue History
Date Modified Username Field Change
2018-07-03 15:04 evdenis New Issue
2018-07-04 09:14 evdenis Note Added: 0006567
2018-07-04 09:15 evdenis File Added: escape_sequences.c
2018-07-04 16:55 yakobowski Assigned To => virgile
2018-07-04 16:55 yakobowski Status new => assigned
2018-07-10 17:04 virgile Note Added: 0006574
2019-06-04 18:24 virgile Status assigned => resolved
2019-06-04 18:24 virgile Resolution open => fixed
2019-06-04 18:24 virgile Fixed in Version => Frama-C 18-Argon
2019-07-05 11:40 signoles Fixed in Version Frama-C 18-Argon => Frama-C 19-Potassium
2019-07-05 11:41 signoles Status resolved => closed
+Issue History