Ich möchte Source Code mit dem Paket Listing (lstlisting) setzen. Ich verwende Annotationen mit Schlüsselworten in Source Code Kommentaren. Die Annotationssprache ist dem Paket bekannt (ACSL). Leider werden diese Schlüsselworte im Kommentar nicht erkannt und nicht entsprechend gesetzt. Ich habe es auch schon mit der Option "alsolanguage" versucht, ohne Erfolg. Wie kann ich Listing dazu bringen, auch die Annotationen korrekt umzusetzen? Unten ein Beispiel. Die Schlüsselworte sind "behavior", "assumes", etc. Vielen Dank im Voraus //@ ghost unsigned int no_btn_press = 0; /*@ @ behavior FewPresses: @ assumes no_btn_press < 2; @ ensures no_btn_press == \old(no_btn_press) + 1; @ ensures \result == 0; @ behavior EnoughPresses: @ assumes no_btn_press >= 2; @ ensures no_btn_press == 0; @ ensures \result != 0; @ complete behaviors FewPresses,EnoughPresses; @ disjoint behaviors FewPresses,EnoughPresses; @*/ char btnpress(void);

Ich möchte Source Code mit dem Paket Listing (lstlisting) setzen. Ich verwende Annotationen mit Schlüsselworten in Source Code Kommentaren. Die Annotationssprache ist dem Paket bekannt (ACSL). Leider werden diese Schlüsselworte im Kommentar nicht erkannt und nicht entsprechend gesetzt. Ich habe es auch schon mit der Option "alsolanguage" versucht, ohne Erfolg. Wie kann ich Listing dazu bringen, auch die Annotationen korrekt umzusetzen? Unten ein Beispiel. Die Schlüsselworte sind "behavior", "assumes", etc. Vielen Dank im Voraus //@ ghost unsigned int no_btn_press = 0; /*@ @ behavior FewPresses: @ assumes no_btn_press < 2; @ ensures no_btn_press == \old(no_btn_press) + 1; @ ensures \result == 0; @ behavior EnoughPresses: @ assumes no_btn_press >= 2; @ ensures no_btn_press == 0; @ ensures \result != 0; @ complete behaviors FewPresses,EnoughPresses; @ disjoint behaviors FewPresses,EnoughPresses; @*/ char btnpress(void);