Fails to reject passing of non-compile-time-known values as arguments to directionless parameters of non-actions #37
Description
Reflects the P4C issue: p4lang/p4c#5405.
The same issue exists in the mechanized P4 spec (the concrete branch), where it fails to reject:
#include <core.p4>
control generic<M>(inout M m);
package top<M>(generic<M> c);
header h_t {
bit<32> f;
}
struct headers_t {
h_t head;
}
extern Counter {
Counter(int size);
void count(bit<8> idx);
}
control c(inout headers_t hdrs) {
Counter(256) ctr;
action a0() {
ctr.count(0);
}
action a1(bit<8> idx) {
ctr.count(idx);
}
table t {
key = { hdrs.head.f : exact; }
actions = { a0; a1; }
}
apply {
t.apply();
}
}
top(c()) main;crt.count(idx); should be rejected because the directionless parameter idx of an action a1 is not a compile-time known value.
However, ./p4spectec run spec-concrete/*.watsup -i p4c/p4include -p program.p4 -rel Program_ok passes without rejection.