- Frama-C is developed by CEA (French nuclear research agency; Inria participated in the beginning of the project, and is still a partner, but development has always been led by CEA);
- Your first-order of approximation is a bit severe; there are formal methods groups within large companies, such as Airbus using Astrée, Frama-C, and CompCet; Framatome (French nuclear reactor business) using Astrée; EDF (French electrical company) using Frama-C; plus several railway companies using formal methods such as B; and NASA, Thales, Scania... It's peanuts compared to the amount of money being poured into blockchains, AI, and the latest hype, but formal methods are used in some industries.
Overall, I agree with you: it's not the best time investment for many SWEs, but if you like maths, formal methods do provide some satisfaction and long-term hope that we'll stop patching bugs and rewriting things all the time, and build some longer-lasting software.
After moving to a newly-finished building, I realized most companies didn't have up-to-date databases and some forms prevented me from correcting the "mis-corrected" addresses. Missed a few deliveries during the first few months/years.
On the other hand, having lived in a country where such databases were notoriously unreliable, such automated processing didn't exist, so I didn't encounter that problem.
Sometimes, having something work "way too well" can lead people to believe it's perfect, and enforce it too strictly.
Every single laptop my company bought me in the last 10 years (3+) had kernel/driver issues, especially with Ubuntu, since the kernel version was usually lower than that from other distros, like Fedora.
This includes mostly graphics driver issues (either simply Nvidia, or hybrids, or some exotic protocols such as DisplayLink), but also touchpad, power/suspend issues (e.g. wake-up failure), lack of fingerprint or smartcard reader drivers... Without mentioning certain manufacturers forcing you to use Windows simply to update docking station firmware drivers (like Dell does).
I still favor Linux whenever I can, but there is a real issue in several models, especially bleeding-edge powerful laptops from brands favored by businesses. Linux certification does improve things, but it often omits "optional" components such as fingerprint readers.
Overall, about 1-2 years after the new laptop model has been released, almost everything works fine, but when you're among the first users, some amount of time will be spent in forums trying to find solutions and workarounds for such issues.
This echoes some vibes of Neal Stephenson's Zodiac. Replace Boston with The Bay, PCBs with VOCs, and fast-forward some 30 years, and there you have it. If only we could learn from past mistakes...
Fixing the Ctrl+Q issue is great, but I still think extensions such as Form History Control are essential for all other situations. I'd very much appreciate if Mozilla could vet it for security; I'm always afraid of some developer selling out or being hacked and a future update introducing a backdoor.
Can you get a long term visa without any job affiliations? I'm not sure that simply having the money is sufficient reason for an European country to give you a long-term visa (> 1 year), depending on which country you come from.
Also, some countries have a "negative privilege" situation, where even if you try to get a low-wage job, you'll have less priority than others, or your employer will need to pay an extra fee to be able to hire you. Many will resort to illegal employment to avoid that.
And do not forget issues about guarantors: some places are really strict about proving you have the money, and simply making a 1-year rent deposit in advance is not enough.
Overall, even when having the money, some people don't have the "privilege" of being able to spend it as they please, in the country of their preference.
Genius! Good to know it exists, if I need it one day.
For now, I tried patching the timestamp in the binary as suggested by jtvjan, since I saw it before your post. It works, so I'll stick with it for now. But I'll be sure to try this RunAsDate when I need something similar in the future.
Thanks a lot! The page you linked did work; I had to copy the Flash folder elsewhere, used a hex editor to find the timestamp in my Flash.ocx file, then I renamed the original folder to Flash.bak and copied the modified one in its place, and my application works again!
Indeed, the laptop has been disconnected for days. I (or, more precisely, Windows) inadvertently updated to a more recent Flash version containing the "time bomb", so now the application simply checks the system date and decides whether to block it or not.
If I could "sandbox the clock" for this specific application, that might work, but I don't think that it is possible.
I have an old Windows offline desktop application (from circa 2003) that has an embedded Flash component which is necessary for it to run properly. It simply stopped working this morning on my Windows 10.
Resetting the date to yesterday works, but I'd like to avoid it if possible.
Standalone flash players (such as Newgrounds') do not work, since the desktop application is the one who actually runs the Flash component, and I cannot control it directly.
I tried uninstalling Flash and reinstalling an older version, without success: it seems to be using an ActiveX component which I cannot overwrite, since the old installer says "You already have a newer version". Windows does not allow me uninstalling it manually (it's "part of the system", and apparently the only Windows Update KB which allows it to be uninstalled, prevents you from installing any other Flash version), and I tried manually searching for registry keys, but there are several and I need to change permissions, etc.
So, I'm afraid I'll have to run an emulator such as PCem, with an older Windows inside, whose date is set to a distant past, so that my app will simply keep working as usual. I'd appreciate if there are simpler solutions.
OCaml is good for handling abstract syntax trees (strong typing, pattern matching) and its mix of imperative and functional programming don't require using borrow-checker nor monads. You can also consider Reason, if you prefer a more C-like syntax.
Would you mind telling some of the kinds of checks the Clang tools do not perform? I wonder if they are mostly syntactic or if they need dataflow analyses. (That said, Polyspace has 2 tools now, Bug Finder and Code Prover, whose applications are somewhat different.)
Which seems interesting, however when I tried the FreeType example, there seemed to be some preprocessing issue, such that some function definitions are conditionally excluded even though they are called later. I didn't have the time to find out if this was an issue in the original code or if the amalgamation script introduced it.
In any case, such single-C programs are very useful for quickly testing tools, so having more of them would be great.
I had never heard of LSIF. Its webpage says it intends to "define a standard format for language servers or other programming tools to dump their knowledge about a workspace". SARIF being targeted towards static analysis tools results, it seems more straightforward to support it both for producing results and for reading them.
To be honest, since both formats are at least partially developed by Microsoft, they might have some common people behind them, but as a user and producer of static analysis tools, I'd prefer to have a single standard. SARIF is already standardized and gaining traction, so it seems the better choice for now.
> I'm at work and not allowed to read active patents.
Is that related to legal issues (as in, if you don't read patents, there's less chance that you'll end up being prosecuted if you accidentally implement something similar)?
- Frama-C is developed by CEA (French nuclear research agency; Inria participated in the beginning of the project, and is still a partner, but development has always been led by CEA);
- Your first-order of approximation is a bit severe; there are formal methods groups within large companies, such as Airbus using Astrée, Frama-C, and CompCet; Framatome (French nuclear reactor business) using Astrée; EDF (French electrical company) using Frama-C; plus several railway companies using formal methods such as B; and NASA, Thales, Scania... It's peanuts compared to the amount of money being poured into blockchains, AI, and the latest hype, but formal methods are used in some industries.
Overall, I agree with you: it's not the best time investment for many SWEs, but if you like maths, formal methods do provide some satisfaction and long-term hope that we'll stop patching bugs and rewriting things all the time, and build some longer-lasting software.