>>109593295
C with ACSL is much safer than Rust
#include <stddef.h>
#include "equal.acsl"
unsigned int count_a(const char *pStr);
/*@
@requires pStr != \null;
@requires \length(pStr) >= 0;
@requires \valid_read(pStr + (0 .. \length(pStr) - 1));
@ensures \result == \count(pStr, 'a');
@ensures \result >= 0;
@assigns \nothing;
*/
unsigned int count_a(const char *pStr)
{
/*
loop invariant 0 <= i <= \length(pStr);
loop invariant count == \count(pStr, pStr[i], 'a');
loop variant \length(pStr) - i;
*/
unsigned int count = 0;
for (size_t i = 0; pStr[i] != '\0'; i++)
{
if (pStr[i] == 'a')
{
count++;
}
}
return count;
}
int main()
{
char *pStr = "xxaxxxxaxxxxxxxxxaxxxxaaxxxxxaaaxxxxxxxaxxxxaaxxxxxxxxxxxxxxxaxxxaaaxxxxxxx";
count_a(pStr);
}
#ifndef EQUAL_ACSL_INCLUDED
#define EQUAL_ACSL_INCLUDED
equal.acsl
/*@
logic integer
Count(char* a, integer m, integer n, char v) =
n <= m ? 0 : Count(a, m, n-1, v) + (a[n-1] == v ? 1 : 0);
logic integer
Count(char* a, integer n, char v) = Count(a, 0, n, v);
*/
#endif