What happens if a function allocates not deterministically, like

if (turing_machine_halts(tm)) return malloc(1); else return NULL;

How is this handled?

NULL is a valid return for malloc. Wouldn’t that case already be handled?

In general, symbolic execution will consider all code paths. If it can't (or doesn't want to) prove that the condition is always true or false it will check that the code is correct in two cases: (1) true branch taken, (2) false branch taken.

I understand how this works in general. I had static analyzers at Uni, I know lattice theory and all this - I am just wondering how Xr0 handles it.

as someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.

Rust is the poster child for these complaints, but this is a great example of "the language rejects a valid program". Not all things that can be expressed in C are good ideas!

This is "valid" C, but I wholly support checking tools that reject it.

exactly! "guaranteeing the safety of C" sir what did you think that meant, sprinkling magic fairy dust to make it work!!?

i made a quip and realized that's not a bad description of what fil-c does

Are you implying that Fil-C has this sort of reaction to people confused about why it does certain things in the name of safety, or are you saying Fil-C is just sprinkling magic fairy dust on C and declaring it safe?

i like fil-c, so i would say "fil c sprinkles magic fairy dust on C and makes it safe (at the cost of perf and elevated risk of crashing)

> just analyze all possible branches and seek convergence.

This sounds like a very simple form of abstract interpretation, how do you handle the issues it generally brings?

For example if after one branch you don't converge, but after two you do, do you accept that? What if this requires remembering the relationship between variables? How do you represent these relationships?

Historically this has been a tradeoff between representing the state space with high or perfect precision, which however can require an exponential amount of memory/calculations, or approximate them with an abstract domain, which however tend to lose precision after performing certain operations.

Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.

> For example if after one branch you don't converge, but after two you do, do you accept that?

you should refactor so that it's representable.

> Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.

regions are hard. You kinda have to reject regions that are not uniform. loops you can find a fixpoint for.

There will always be valid programs that are nonetheless rejected by some verifier (Rice's theorem). That is, programs that have really nothing wrong but nonetheless are rejected as invalid

In those cases you generally try to rewrite it in another way

I think all paths have to return the same allocation. You would have to solve this in another way.

Isn’t this a very restrictive way to write? Hard for me to imagine as never wrote with such annotations so no idea how viable it is for a large codebase to have this constraint.

Sure, but you want restrictions. You can't get an annotation that magically eliminates (de)allocation errors. It comes at a cost. The advantage of this particular proposal is its simplicity, I think. Otherwise, you'd have to get into contracts with complex expressions and then you'll have to prove those expression hold, and before you know it, your program is filled with proof statements. At least, that's my (limited) experience in SPARK, where you even can't have pointers.

My point is can you write a json deserializer with this, where allocation of every child is defacto optional, depending on input JSON?

As long as the verifier can be satisfied by wrapping the different results in a common type you should be fine. There has to be some way to appease it in that scenario as otherwise even trivial programs wouldn't be able to pass.

For the bootstrap c lexer and parser was hand rolling really necessary? Lex and yacc exist for a reason

Bro no one will use a web service and trust it is 100% private. This is an unprovable claim. Maybe it is private now, but you sell this in 5 years and it stops being so.

Maybe a JavaScript ad jailbreaks an iframe and reads this.

There is no beating a locally running program

Agreed the feeling of pasting code to external website always feels insecure. But it doesn't mean locally running programs are safe either.

Atleast in website like this you can disable network access and work in offline mode and get the confident.

But most CIs allow flaky tests :)

Isn’t this like argparse from Python for typescript?

What OP calls an "combinatorial parser" I'd call object schema validation and that's more similar to pydantic[0] than argparse in python land.

[0]: https://docs.pydantic.dev/latest/

So, typer than

Or click

Couldn’t they add a ChatGPT like bot that would answer questions about confluence or jira content as first AI feature instead of adding unhelpful chatbots for customer support

Is this a replacement for a huge corpo botnet like access control?

If I am a huge corpo, don’t I want to have another huge corpo provide me the software with a support package to have some asssurance and not go with the open source option?

Not sure if your project solves any issue of a singular dev.

Octelium itself is designed to be a generic secure access platform that can operate in many environments (from a simple ngrok-tier remote access tool, remote access/corporate VPN up to a full-fledged scalable ZTNA/BeyondCorp platform among many other specific use cases such as API/AI/MCP gateways) at many levels (i.e. dev, startup, enterprise). Think of Kubernetes, you can use it to host a single website running on a single container, you can use it as an API gateway for a few microservices and you can use it as a fully-featured service mesh of hundreds if not thousands of microservices running on tens if not hundreds of nodes with enterprise-level tools such as SPIFFE, Istio, etc...

Can you show how it works on the page or readme as a video?

Does it open pager or editor? How does it show the shellcheck issues.

You're right, the README explains what vet does, but it doesn't do a great job of showing how it feels to use it. I'll definitely create a demo GIF for the page.

To answer your questions directly in the meantime:

- Pager or Editor? It opens a pager (less by default, but it will automatically use the much nicer bat if you have it installed for syntax highlighting). It doesn't open an editor to prevent any accidental modifications.

- ShellCheck Issues: If shellcheck finds issues, it prints its standard, colorful output directly to your terminal before you review the script. It then pauses and asks you if you want to proceed with the review despite the warnings, like this:

==> Running ShellCheck analysis...

In /tmp/tmp.XXXXXX line 7: echo "Processing file: $filename" ^-- SC2086: Double quote to prevent globbing and word splitting.

==> WARNING: ShellCheck found potential issues. [?] Continue with review despite issues? [y/N]

Thanks again for the excellent idea!

The author declared no competing interests, but I bet they are a certified cat lover and therefore biased

They're secretly funded by Big Cat.