c-semantics

c-semantics copied to clipboard

Much of the C semantics was written long ago, when the K framework did not support many of its current features and was buggy. Now we should be able to replace rules of the form

rule compositeFunctionType(T:Type, Mods:Set, .K, P:List, .List, _)
  => compositeFunctionType(T, Mods, .K, .List, .List, P)
requires P =/=K .List

with

rule compositeFunctionType(T:Type, Mods:Set, .K, `P:List => .List`, .List, `_ => P`)
requires P =/=K .List

This is more compact and potentially faster and more concurrent.

This is not urgent, but it may be worth beautifying a bit the C semantics at some later point. Maybe have some intern or someone interested in learning the C semantics do it? Any volunteer?