Isabelle C-Parser refuses to handle string literals.

[gteege]

When a Cogent program stringconst.cogent such as

f : String -> ()

g: () -> ()
g () = f "abc"

is compiled to C and loaded in Isabelle the C-Parser signals an error:

*** .../stringconst.c:15.15-15.20: Don't want to handle string literals!
*** 
*** At command "install_C_file" (line 14 of "...")

I am using Autocorres Version 1.5 (10 September 2018) and the C-Parser included there.

[zilinc]

Yes you are right. The verification toolchain does not support strings, but the language supports strings anyway for writing debugging functions.