2021-02-24 19:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002146Frama-CKernelpublic2016-08-29 17:26
Reporterdcok@grammatech.com 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002146: Frama-C does not support standard C digraphs
DescriptionFrama-C does not parse a program like


void func() <%
    return;
%>

Presumably other standard digraphs and trigraphs are not supported as well.
TagsNo tags attached.
Attached Files
  • patch file icon clexer.mll.patch (906 bytes) 2015-07-28 17:46 -
    --- clexer.mll.orig	2015-07-28 17:41:56.468046340 +0200
    +++ clexer.mll.patched	2015-07-28 17:42:04.968030524 +0200
    @@ -565,6 +565,7 @@
                                               initial lexbuf
                                             }
     |		'#'			{ hash lexbuf}
    +|		"%:"			{ hash lexbuf}
     |               "_Pragma" 	        { PRAGMA (currentLoc ()) }
     |		'\''			{ CST_CHAR (chr lexbuf, currentLoc ())}
     |		"L'"			{ CST_WCHAR (chr lexbuf, currentLoc ()) }
    @@ -635,8 +636,12 @@
     
     |		'{'		       {dbgToken (LBRACE (currentLoc ()))}
     |		'}'		       {dbgToken (RBRACE (currentLoc ()))}
    +|		"<%"		       {dbgToken (LBRACE (currentLoc ()))}
    +|		"%>"		       {dbgToken (RBRACE (currentLoc ()))}
     |		'['				{LBRACKET}
     |		']'				{RBRACKET}
    +|		"<:"				{LBRACKET}
    +|		":>"				{RBRACKET}
     |		'('		       {dbgToken (LPAREN (currentLoc ())) }
     |		')'				{RPAREN}
     |		';'		       {dbgToken (SEMICOLON (currentLoc ())) }
    
    patch file icon clexer.mll.patch (906 bytes) 2015-07-28 17:46 +

-Relationships
+Relationships

-Notes

~0005988

maroneze (administrator)

Just a clarification: trigraphs are supported, since they are processed by the C preprocessor (e.g. with -cpp-extra-args="-trigraphs" if using GCC), but the digraphs defined in the C99 standard are not currently supported.

~0005989

maroneze (administrator)

After a quick glance, it seems that patching src/cil/frontc/lexer.mll could work, at least for a few toy examples I tried it on (such as your example code).

The attached patch (for Frama-C Sodium) should allow you to perform some tests.

More robust testing would be required before merging this intro trunk, however.

~0006257

maroneze (administrator)

C99 digraphs are now supported in Frama-C.
+Notes

-Issue History
Date Modified Username Field Change
2015-07-16 17:40 dcok@grammatech.com New Issue
2015-07-16 17:40 dcok@grammatech.com Status new => assigned
2015-07-16 17:40 dcok@grammatech.com Assigned To => virgile
2015-07-28 17:26 maroneze Note Added: 0005988
2015-07-28 17:46 maroneze File Added: clexer.mll.patch
2015-07-28 17:48 maroneze Note Added: 0005989
2015-07-28 17:53 maroneze Assigned To virgile => maroneze
2015-07-28 17:53 maroneze Status assigned => confirmed
2015-07-28 18:40 maroneze Category Kernel > ACSL implementation => Kernel
2016-08-25 13:42 maroneze Note Added: 0006257
2016-08-25 13:42 maroneze Status confirmed => resolved
2016-08-25 13:42 maroneze Fixed in Version => Frama-C Aluminium
2016-08-25 13:42 maroneze Resolution open => fixed
2016-08-29 17:26 maroneze Status resolved => closed
+Issue History