search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

fixed printing clight identifiers. #329

Closed nikaido-shinku closed 2 years ago

nikaido-shinku commented 2 years ago

The name_of_ident function is relocated in Compcert 3.10. Also, I'm not sure if I should open a pull request for this kind of small changes, but I opened it anyway just for safety.

hackedy commented 2 years ago

Looks good. Do we have any way to test this besides manually inspecting the compiler output?

nikaido-shinku commented 2 years ago

Looks good. Do we have any way to test this besides manually inspecting the compiler output?

Yes, at least in some way. Running make ctest will output error if the identifier was not printed as string, since it would be a syntactically invalid c program. So if there's no error in make ctest, the identifiers should be printed out as string.