Support for parsing extended assembly code including `asm goto`

[WernerDrasche]

See #81

[WernerDrasche]

• The main.ml changes were unintentionally forgotten testing utilities.
• asmlabelslst_ne is not used in first step because we semantically distinguish between:
  • labels field was provided (Some [...])
  • labels field was omitted (None)
• the check asm function ensures that goto attribute <=> labels field (otherwise we would need state in the parser). it doesn't return unit because for whatever reason when I write in cparser.mly inside asm rule: { let asm = ASM ($1 ....) in checkAsm asm; asm } dune build fails with a syntax error in cparser.ml (can't really debug that because it's generated.
• as cil cfg is only used to make the goblint cfg, we don't do anything special for the cil one
• ASM a does not work for some reason (replying to the comment in email)
• I don't know what to do for the dummy instruction (do we need to introduce a new instruction type for that?)

[WernerDrasche]

The dummyInstr can be safely deleted from cil.mli I think, as after grepping for it inside gobling-analyzer and goblint-cil no matches were found. Otherwise I have no clue on how to implement a dummy instruction using either set | vardecl | call.

[michael-schwarz]

It would be good to include additional tests for the new features.

I think has not been addressed yet, if I see correctly?

[michael-schwarz]

The dummyInstr can be safely deleted from cil.mli I think, as after grepping for it inside gobling-analyzer and goblint-cil no matches were found. Otherwise I have no clue on how to implement a dummy instruction using either set | vardecl | call.

I think it would still be useful to keep it, as there are other users of goblint-cil. Maybe you can add a vardecl instruction for a new dummy variable? I think this is the best option.

[michael-schwarz]

Also, feel free to mark suggestions that you have implemented and there's nothing more to discuss as resolved, that makes it easier for us to keep track of what remains still TODO.

[michael-schwarz]

The currently still failing task is CC=gcc make test/asm_goto3.

[michael-schwarz]

The error message is

Entering directory '/home/michael/Documents/goblint-cil/cil'
cd ./small1; /home/michael/Documents/goblint-cil/cil/_build/default/test/../bin/cilly --mode=GNUCC --decil --save-temps  --strictcheck --stats --nomerge --commPrintLn \
       -c -std=gnu90 -D_GNUCC -Wall -g -ggdb -D_DEBUG -S -o asm_goto3.s asm_goto3.c
First CIL check
Timings:
TOTAL                           0.001 s
  parse                           0.000 s
  convert to CIL                  0.000 s
  printCIL                        0.000 s
Timing used
Memory statistics: total=5.10MB, max=1.02MB, minor=4.93MB, major=0.91MB, promoted=0.74MB
    minor collections=4  major collections=0 compactions=0
./asm_goto3.cil.c: In function ‘code’:
./asm_goto3.cil.c:15:30: error: expected identifier before ‘)’ token
   __asm__  goto   ("nop": : : : );
                              ^
Makefile:175: recipe for target 'test/asm_goto3' failed
make: *** [test/asm_goto3] Error 1

[michael-schwarz]

/* Generated by Goblint-CIL v. %%VERSION_NUM%% */
/* print_CIL_Input is false */

//#line  3 "testharness.h"
extern int printf(char const   *format  , ...) ;
//#line  12
extern void exit(int  ) ;
//#line  3 "asm_goto3.c"
void code(void) 
{ 

  {
//#line  5
  __asm__  goto   ("nop": : : : );
//#line  7
  printf((char const   *)"Success\n");
//#line  7
  exit(0);
}
}

This the produced C program.

[michael-schwarz]

And the error message is

gcc small1/asm_goto3.cil.c
small1/asm_goto3.cil.c: In function ‘code’:
small1/asm_goto3.cil.c:15:33: error: expected identifier before ‘)’ token
   __asm__  goto   ("nop": : : : );
                                 ^