%{^
#include "ats_counter.cats" /* only needed for [ATS/Geizella] */
%}
staload Cnt = "ats_counter.sats"
staload "ats_stamp.sats"
assume stamp_t = $Cnt.count_t
implement
lt_stamp_stamp (s1, s2) = $Cnt.lt_count_count (s1, s2)
implement
lte_stamp_stamp (s1, s2) = $Cnt.lte_count_count (s1, s2)
implement
eq_stamp_stamp (s1, s2) = $Cnt.eq_count_count (s1, s2)
implement
neq_stamp_stamp (s1, s2) = $Cnt.neq_count_count (s1, s2)
implement
compare_stamp_stamp (s1, s2) = $Cnt.compare_count_count (s1, s2)
implement fprint_stamp (pf | out, s) = $Cnt.fprint_count (pf | out, s)
implement print_stamp (s) = print_mac (fprint_stamp, s)
implement prerr_stamp (s) = prerr_mac (fprint_stamp, s)
implement tostring_stamp (s) = $Cnt.tostring_count (s)
local val counter = $Cnt.counter_make () in
implement s2rtdat_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement s2cst_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement s2var_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement s2Var_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement s2exp_struct_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement s2exp_union_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement d2con_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement d2cst_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement d2mac_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement d2var_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement funlab_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement tmplab_stamp_make () = $Cnt.counter_get_and_inc counter
end
local val counter = $Cnt.counter_make () in
implement tmpvar_stamp_make () = $Cnt.counter_get_and_inc counter
end